COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Computing with Symbolic Expressions
C00007 00003		Most students of programming begin with a language oriented
C00010 00004
C00021 00005	.s(PREFAC, INTRODUCTION)
C00028 ENDMK
C⊗;
Computing with Symbolic Expressions
	notation
The LISP language
	the province of LISP
	Macsyma, Reduce and Scratchpad
	can it be written at all
Pure LIsp
	recursive functions of symbolic expressions
Program proving
	applied goal of proving
	understanding the programs
	extension beyond present limitations
	computability and connections with logic and recursive function theory
extended LISP
	macros, pattern directed computation
applications
	compiling, pattern directed computation, tree search
what about the poor student
	learn to program in pure LISP - a new style
	learn to prove assertions about programs
	learn about programs that produce program

.if false then begin
computing with symbolic expressions
lisp as a programming language

internal and external notation

proving programs
lisp has been most useful when the difficulty is not in making the
program fast but in making it very sophisticated
Can it be written at all.

We believe that experience in proving that programs meet specifications
will benefit the student's clarity of understanding even if he doesn't
subsequently prove programs.

"Proving that programs meet their specifications" and "proving
assertions about programs" are long phrases that tend to be abbreviated
to "proving programs".  However, we need to be clear that a program by
itself is not an assertion that can be proved or disproved; it is more
like a definition.  What is proved is an assertion about the program,
and it is sometimes quite problematical what assertions are appropriate
to prove about a give program and how to express them formally.

LISP has a core called pure LISP about which mathematical reasoning is
especially well developed.

*****
	While the first computers were intended for numerical computation,
computing with symbolic expressions began as soon as memories were
large enough to do toy problems.  Nevertheless, 

	The LISP programming language is intended for computing with
symbolic expressions.  Symbolic computations are important 
.end


Computing with Symbolic Expressions

	The first computers were built to do numerical computation, and
for many years, no-one has done extended numerical computation by hand.
There are pocket calculators, programmable hand held calculators, small
computer systems with BASIC, time-sharing systems, and large number
crunchers like the Cray-1.  Symbolic computation has proved harder.

	Though the first machine computations with symbolic expressions
were done in the early 1950s and programming languages for symbolic
computation were developed in the late 1950s, people still cover many
sheets of paper wiih hand symbolic computations.

	Most students of programming begin with a language oriented
towards computing with numbers.  LISP is oriented toward computing
with symbolic expressions.

	While the first efforts at computing with symbolic expressions
began in the early 1950s, and LISP and other languages for symbolic
computation were developed by 1960, symbolic computation has proved
intrinsically more difficult than numerical computation.
No-one does numerical computation by hand today, but most algebraic
computation is still done by hand on paper.  This is partly because
the existing large scale algebraic systems are not widely available,
partly because their features are useful for only certain classes
of problems, and partly because symbolic computation involves often
involves ingenuity that applied to special situations that artificial
intelligence has not yet been able to make routinely available to
programs.

	The best developed form of symbolic computation is compiling,
partly because it is straightforward, and partly because computer
scientists tend to act according to the principle that charity begins
at home.

	In choosing a notation for some kind of symbolic expressions,
there are three objectives which are usually not completely
compatible.  One would like the notation to be readable, and this
is aided by good typography including judicious use of several type
fonts.  One would like it to be conveniently writeable, and this usually
precludes multiple fonts.  The third objective is that it should
be convenient to write programs that manipulate expressions in
the notation.  LISP is optimized for meeting this last requirement.


The LISP Language

	LISP was developed between 1958 and 1960 mainly for work in
artificial intelligence.

This Textbook
.s(PREFAC, INTRODUCTION)


	This book covers recursive programming in LISP, computation
with symbolic expressions represented by LISP S-expressions,
representation of S-expressions by list structure in the memory
of a computer, and techniques for mathematically proving that programs meet
their specifications.  We cover the following main topics.

1. Writing recursive programs.  Most students will have already
learned to write sequential programs which change an initial state
of a computation to reach a state satisfying a desired condition.
Recursive programming requires inventing functions that give the
answer in terms of the initial information by building it up from
already available functions and simpler cases of the function
being defined.  Either kind of
program is universal, and the two programming styles are complementary.
The kind of recursion that makes good programs is %2conditional
expression recursion%1 which differs in important respects
from the recursive definitions
familiar to mathematicians.

2. Computing with symbolic expressions represented by list structure
in the memory of a computer.  The LISP S-expressions form a data domain
with a simple and regular structure, and important computations
with symbolic expressions are readily represented as functions
defined by conditional expression recursion.
The examples are taken from tree search, computing with algebraic
and other expressions involving elementary functions,
pattern matching,
and compiling, interpreting and transforming recursive programs.
Recursive programming is the main technique, but sequential
programs are also discussed.

	The student who has completed a course based on this book
should be able to use LISP proficiently for symbolic computation and
in artificial intelligence applications.

3. Proving programs correct.  A major applied task of computer science
is to develop mathematical theory of computation to the point where
a program is not considered complete until it has been proven to
meet its specification and this proof has been checked by a proof-checker
program.  In particular, a university level course in programming
for computer science students should
teach them to prove correct the programs they write in the course.

	While program proving has not advanced to the point where
it can replace debugging most programs, it has advanced to the point
where it should be studied by all comptter science students.

	We include techniques for proving the extensional
correctness of recursive programs in pure LISP, and most of the
programming exercises are within easy range of these techniques.
Thus recent Stanford
examinations have included programming problems together with a
requirement that the solution be proved to meet certain specifications.
Some techniques are available for non-extensional properties such
as the number of operations executed, and some are available for
sequential programs.

	Recursive programs are represented as functions in a first
order theory and are defined by a %2functional equation%1 which is
essentially a copy of the recursive definition and by a %2minimization
schema%1 which is a sentence schema of first order logic with a
free function parameter.  When the function is total the schema can
be dispensed with.  The extensional properties proved are then just
sentences in first order logic, and its familiar apparatus is
available for proofs.  The technique is much more direct and easier
to use than the methods available for sequential programs
such as %2inductive assertions%1 and the Hoare axiomatization.

	In fact the proofs are
readily computer-checked by Richard Weyhrauch's experimental first order
proof-checker FOL.
We may be able to include computer proof-checking in a future version
of the course and a future edition of the book.

	Additional theoretical topics include the universal LISP function,
%2eval%1 which also serves as a LISP interpreter, %2abstract syntax%1
which enables convenient proofs of the correctness of a simple compiler,
an introductory discussion of computability and an introduction to
the lambda calculus.

	An additional applied topic is pattern directed computation.